|
Java Pathfinder (JPF) is a system to verify executable Java bytecode programs. JPF was developed at the NASA Ames Research Center and open sourced in 2005. The acronym JPF is not to be confused with the unrelated ''Java Plugin Framework'' project. The core of JPF is a Java Virtual Machine that is also implemented in Java. JPF executes normal Java bytecode programs and can store, match and restore program states. Its primary application has been Model checking of concurrent programs, to find defects such as data races and deadlocks. With its respective extensions, JPF can also be used for a variety of other purposes, including * model checking of distributed applications * model checking of user interfaces * test case generation by means of symbolic execution * low level program inspection * program instrumentation and runtime monitoring JPF has no fixed notion of state space branches and can handle both data and scheduling choices. == Example == The following system under test contains a simple race condition between two threads accessing the same variable d in statements (1) and (2), which can lead to a division by zero exception if (1) is executed before (2)static void doSomething (int n) } } Without any additional configuration, JPF would find and report the division by zero. If JPF is configured to verify absence of race conditions (regardless of their potential downstream effects), it will produce the following output, explaining the error and showing a counter example leading to the error 抄文引用元・出典: フリー百科事典『 ウィキペディア（Wikipedia）』 ■ウィキペディアで「Java Pathfinder」の詳細全文を読む スポンサード リンク
|